基于布尔可满足性问题（SAT）的自动化搜索方法可以直接刻画与、或、非、异或等逻辑运算，从而建立更高效的搜索模型。为更高效地评估GRANULE算法抵抗不可能差分攻击的能力，首先，基于S盒差分分布表性质优化S盒差分性质刻画的SAT模型；其次，对GRANULE算法建立基于比特的不可能差分区分器的SAT模型，通过求解模型得到多条10轮GRANULE算法的不可能差分区分器；再次，针对不可能差分区分器，给出改进的SAT自动化验证方法并验证；最后，将得到的区分器往前和往后各扩展3轮，对GRANULE-64/80算法发起16轮的不可能差分攻击，通过该攻击可以恢复80比特主密钥，时间复杂度为251.8次16轮加密，数据复杂度为241.8个选择明文。与表现次优的对GRANULE算法不可能差分分析的方法相比，所得到的区分器轮数和密钥恢复攻击轮数都提高了3轮，且时间复杂度、数据复杂度都进一步下降。
